Require Import NaturalDeduction.

Lemma Question1 (A : Type) (P : A -> Prop) : ~(exists x, ~P x) <-> forall x, P x.
Proof.
   unfold iff.
   And_Intro.
   Impl_Intro.
   Forall_Intro.
   PBC.
   assume (exists x : A, ~ P x).
   Not_Elim in H and H1.
   assumption.
   Exists_Intro with x.
   assumption.
   Impl_Intro.
   Not_Intro.
   Exists_Elim in H0.
   Forall_Elim in H with x.
   Not_Elim in H1 and H3.
   assumption.
Qed.

Lemma Question2 (A : Type) (P : A -> Prop) (Q R : A -> A -> Prop) : (forall x, P x /\ (exists y, Q x y /\ R x y)) -> (forall x, P x) /\ (forall x, (exists y, Q x y) /\ (exists y, R x y)).
Proof.
  Impl_Intro.
  And_Intro.
  Forall_Intro.
  Forall_Elim in H with x.
  And_Elim_1 in H1.
  assumption.
  Forall_Intro.
  Forall_Elim in H with x.
  And_Elim_2 in H1.
  And_Intro.
  Exists_Elim in H0.
  Exists_Intro with x0.
  And_Elim_1 in H2.
  assumption.
  Exists_Elim in H0.
  Exists_Intro with x0.
  And_Elim_2 in H2.
  assumption.
Qed.

(* 
Question 3:
Show that the converse implication of Question 2, i.e., the formula
(forall x, P x) /\ (forall x, (exists y, Q x y) /\ (exists y, R x y)) ->  (forall x, P x /\ (exists y, Q x y /\ R x y)).
is not valid.
Hint: A model with two elements is sufficient.

Solution:
Let |M|={1,2}, P^M={1,2}, Q^M={(1,1),(2,1)}, and R^M={(1,2),(2,2)}. Then M |= forall x, P x. Furthormore,
M |= exists y, Q x y [\sigma[1/x]] since M |= Q x y [\sigma[1/x][1/y] and
M |= exists y, Q x y [\sigma[2/x]] since M |= Q x y [\sigma[2/x][1/y]. Analogously, we have
M |= exists y, R x y [\sigma[1/x]] since M |= R x y [\sigma[1/x][2/y] and
M |= exists y, R x y [\sigma[2/x]] since M |= Q x y [\sigma[2/x][2/y].
Therefore, M |= (forall x, (exists y, Q x y) /\ (exists y, R x y)), and, hence, the left-hand side of the implication.
On the other hand, M |= (exists y, Q x y /\ R x y) [\sigma[1/x]] is not true, i.e., the right-hand side of the 
implication is false.

*)